CHOICE-STRATEGY-IS: 
ANCESTRY∧SUPPORT[THM]∧EQUALITY[=,3];

EDIT-STRATEGY-IS: 
DEMOD[4,3,2,1;4]∧(DEPTH[3]∨LENGTH[1]);

ELAPSED-TIME =1734

NIL 1 2
1 (x ⊗(y ⊗ z))=(z ⊗(y ⊗ x));G3
2 ¬((THM2 ⊗ THM1)⊗(THM3 ⊗ THM1))=(THM2 ⊗ THM3);THM